YES 1.252 H-Termination proof of /home/matraf/haskell/eval_FullyBlown_Fast/empty.hs
H-Termination of the given Haskell-Program with start terms could successfully be proven:



HASKELL
  ↳ BR

mainModule Main
  ((notElem :: Eq a => a  ->  [a ->  Bool) :: Eq a => a  ->  [a ->  Bool)

module Main where
  import qualified Prelude



Replaced joker patterns by fresh variables and removed binding patterns.

↳ HASKELL
  ↳ BR
HASKELL
      ↳ COR

mainModule Main
  ((notElem :: Eq a => a  ->  [a ->  Bool) :: Eq a => a  ->  [a ->  Bool)

module Main where
  import qualified Prelude



Cond Reductions:
The following Function with conditions
undefined 
 | False
 = undefined

is transformed to
undefined  = undefined1

undefined0 True = undefined

undefined1  = undefined0 False



↳ HASKELL
  ↳ BR
    ↳ HASKELL
      ↳ COR
HASKELL
          ↳ Narrow

mainModule Main
  (notElem :: Eq a => a  ->  [a ->  Bool)

module Main where
  import qualified Prelude



Haskell To QDPs


↳ HASKELL
  ↳ BR
    ↳ HASKELL
      ↳ COR
        ↳ HASKELL
          ↳ Narrow
            ↳ AND
QDP
                ↳ QDPSizeChangeProof
              ↳ QDP
              ↳ QDP
              ↳ QDP
              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primPlusNat(Succ(xv1400), Succ(xv401000)) → new_primPlusNat(xv1400, xv401000)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ BR
    ↳ HASKELL
      ↳ COR
        ↳ HASKELL
          ↳ Narrow
            ↳ AND
              ↳ QDP
QDP
                ↳ QDPSizeChangeProof
              ↳ QDP
              ↳ QDP
              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primMulNat(Succ(xv3100), Succ(xv40100)) → new_primMulNat(xv3100, Succ(xv40100))

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ BR
    ↳ HASKELL
      ↳ COR
        ↳ HASKELL
          ↳ Narrow
            ↳ AND
              ↳ QDP
              ↳ QDP
QDP
                ↳ QDPSizeChangeProof
              ↳ QDP
              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primEqNat(Succ(xv300), Succ(xv4000)) → new_primEqNat(xv300, xv4000)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ BR
    ↳ HASKELL
      ↳ COR
        ↳ HASKELL
          ↳ Narrow
            ↳ AND
              ↳ QDP
              ↳ QDP
              ↳ QDP
QDP
                ↳ QDPSizeChangeProof
              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_esEs0(@3(xv30, xv31, xv32), @3(xv400, xv401, xv402), df, dg, app(app(ty_@2, eg), eh)) → new_esEs3(xv32, xv402, eg, eh)
new_esEs0(@3(xv30, xv31, xv32), @3(xv400, xv401, xv402), app(app(ty_Either, gd), ge), dg, fc) → new_esEs(xv30, xv400, gd, ge)
new_esEs3(@2(xv30, xv31), @2(xv400, xv401), bbh, app(ty_Maybe, bcg)) → new_esEs2(xv31, xv401, bcg)
new_esEs0(@3(xv30, xv31, xv32), @3(xv400, xv401, xv402), app(ty_[], ha), dg, fc) → new_esEs1(xv30, xv400, ha)
new_esEs0(@3(xv30, xv31, xv32), @3(xv400, xv401, xv402), app(ty_Maybe, hb), dg, fc) → new_esEs2(xv30, xv400, hb)
new_esEs0(@3(xv30, xv31, xv32), @3(xv400, xv401, xv402), df, dg, app(ty_Maybe, ef)) → new_esEs2(xv32, xv402, ef)
new_esEs2(Just(xv30), Just(xv400), app(app(ty_Either, bag), bah)) → new_esEs(xv30, xv400, bag, bah)
new_esEs0(@3(xv30, xv31, xv32), @3(xv400, xv401, xv402), df, app(ty_[], fh), fc) → new_esEs1(xv31, xv401, fh)
new_esEs(Right(xv30), Right(xv400), cc, app(app(app(ty_@3, cf), cg), da)) → new_esEs0(xv30, xv400, cf, cg, da)
new_esEs(Right(xv30), Right(xv400), cc, app(ty_[], db)) → new_esEs1(xv30, xv400, db)
new_esEs0(@3(xv30, xv31, xv32), @3(xv400, xv401, xv402), df, dg, app(app(ty_Either, dh), ea)) → new_esEs(xv32, xv402, dh, ea)
new_esEs1(:(xv30, xv31), :(xv400, xv401), he) → new_esEs1(xv31, xv401, he)
new_esEs(Right(xv30), Right(xv400), cc, app(app(ty_@2, dd), de)) → new_esEs3(xv30, xv400, dd, de)
new_esEs3(@2(xv30, xv31), @2(xv400, xv401), app(app(app(ty_@3, bde), bdf), bdg), bdd) → new_esEs0(xv30, xv400, bde, bdf, bdg)
new_esEs1(:(xv30, xv31), :(xv400, xv401), app(ty_[], bac)) → new_esEs1(xv30, xv400, bac)
new_esEs3(@2(xv30, xv31), @2(xv400, xv401), bbh, app(ty_[], bcf)) → new_esEs1(xv31, xv401, bcf)
new_esEs2(Just(xv30), Just(xv400), app(ty_[], bbd)) → new_esEs1(xv30, xv400, bbd)
new_esEs2(Just(xv30), Just(xv400), app(ty_Maybe, bbe)) → new_esEs2(xv30, xv400, bbe)
new_esEs0(@3(xv30, xv31, xv32), @3(xv400, xv401, xv402), df, app(app(app(ty_@3, fd), ff), fg), fc) → new_esEs0(xv31, xv401, fd, ff, fg)
new_esEs(Left(xv30), Left(xv400), app(app(app(ty_@3, bd), be), bf), bc) → new_esEs0(xv30, xv400, bd, be, bf)
new_esEs3(@2(xv30, xv31), @2(xv400, xv401), app(ty_[], bdh), bdd) → new_esEs1(xv30, xv400, bdh)
new_esEs(Left(xv30), Left(xv400), app(ty_Maybe, bh), bc) → new_esEs2(xv30, xv400, bh)
new_esEs0(@3(xv30, xv31, xv32), @3(xv400, xv401, xv402), df, app(app(ty_@2, gb), gc), fc) → new_esEs3(xv31, xv401, gb, gc)
new_esEs0(@3(xv30, xv31, xv32), @3(xv400, xv401, xv402), df, dg, app(ty_[], ee)) → new_esEs1(xv32, xv402, ee)
new_esEs2(Just(xv30), Just(xv400), app(app(app(ty_@3, bba), bbb), bbc)) → new_esEs0(xv30, xv400, bba, bbb, bbc)
new_esEs3(@2(xv30, xv31), @2(xv400, xv401), bbh, app(app(ty_@2, bch), bda)) → new_esEs3(xv31, xv401, bch, bda)
new_esEs0(@3(xv30, xv31, xv32), @3(xv400, xv401, xv402), app(app(ty_@2, hc), hd), dg, fc) → new_esEs3(xv30, xv400, hc, hd)
new_esEs1(:(xv30, xv31), :(xv400, xv401), app(app(ty_@2, bae), baf)) → new_esEs3(xv30, xv400, bae, baf)
new_esEs(Right(xv30), Right(xv400), cc, app(app(ty_Either, cd), ce)) → new_esEs(xv30, xv400, cd, ce)
new_esEs(Left(xv30), Left(xv400), app(app(ty_@2, ca), cb), bc) → new_esEs3(xv30, xv400, ca, cb)
new_esEs3(@2(xv30, xv31), @2(xv400, xv401), app(ty_Maybe, bea), bdd) → new_esEs2(xv30, xv400, bea)
new_esEs0(@3(xv30, xv31, xv32), @3(xv400, xv401, xv402), df, dg, app(app(app(ty_@3, eb), ec), ed)) → new_esEs0(xv32, xv402, eb, ec, ed)
new_esEs1(:(xv30, xv31), :(xv400, xv401), app(ty_Maybe, bad)) → new_esEs2(xv30, xv400, bad)
new_esEs3(@2(xv30, xv31), @2(xv400, xv401), app(app(ty_@2, beb), bec), bdd) → new_esEs3(xv30, xv400, beb, bec)
new_esEs(Right(xv30), Right(xv400), cc, app(ty_Maybe, dc)) → new_esEs2(xv30, xv400, dc)
new_esEs1(:(xv30, xv31), :(xv400, xv401), app(app(app(ty_@3, hh), baa), bab)) → new_esEs0(xv30, xv400, hh, baa, bab)
new_esEs3(@2(xv30, xv31), @2(xv400, xv401), bbh, app(app(ty_Either, bca), bcb)) → new_esEs(xv31, xv401, bca, bcb)
new_esEs2(Just(xv30), Just(xv400), app(app(ty_@2, bbf), bbg)) → new_esEs3(xv30, xv400, bbf, bbg)
new_esEs3(@2(xv30, xv31), @2(xv400, xv401), app(app(ty_Either, bdb), bdc), bdd) → new_esEs(xv30, xv400, bdb, bdc)
new_esEs(Left(xv30), Left(xv400), app(ty_[], bg), bc) → new_esEs1(xv30, xv400, bg)
new_esEs0(@3(xv30, xv31, xv32), @3(xv400, xv401, xv402), df, app(app(ty_Either, fa), fb), fc) → new_esEs(xv31, xv401, fa, fb)
new_esEs3(@2(xv30, xv31), @2(xv400, xv401), bbh, app(app(app(ty_@3, bcc), bcd), bce)) → new_esEs0(xv31, xv401, bcc, bcd, bce)
new_esEs0(@3(xv30, xv31, xv32), @3(xv400, xv401, xv402), df, app(ty_Maybe, ga), fc) → new_esEs2(xv31, xv401, ga)
new_esEs1(:(xv30, xv31), :(xv400, xv401), app(app(ty_Either, hf), hg)) → new_esEs(xv30, xv400, hf, hg)
new_esEs0(@3(xv30, xv31, xv32), @3(xv400, xv401, xv402), app(app(app(ty_@3, gf), gg), gh), dg, fc) → new_esEs0(xv30, xv400, gf, gg, gh)
new_esEs(Left(xv30), Left(xv400), app(app(ty_Either, ba), bb), bc) → new_esEs(xv30, xv400, ba, bb)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ BR
    ↳ HASKELL
      ↳ COR
        ↳ HASKELL
          ↳ Narrow
            ↳ AND
              ↳ QDP
              ↳ QDP
              ↳ QDP
              ↳ QDP
QDP
                ↳ QDPSizeChangeProof

Q DP problem:
The TRS P consists of the following rules:

new_foldr(xv3, :(xv40, xv41), ba) → new_foldr(xv3, xv41, ba)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs: